(PROGN (LISPXPRIN1 (QUOTE "FILE CREATED ")
                     T)
         (LISPXPRIN1 (QUOTE "24-AUG-73 16:41:15")
                     T)
         (LISPXTERPRI T))
(DEFINEQ

(ADDFNS
  [LAMBDA (FNS)
    (COND
      ((ATOM FNS)
        (SETQ EXAMFNS (MERGE (LIST FNS)
                             EXAMFNS)))
      (T (MERGE (SORT FNS)
                EXAMFNS])

(ASSERT
  [LAMBDA (ASSERTION CONTEXT)
    (COND
      [(EQ CONTEXT (QUOTE GLOBAL))
        (SETQ ASSERTIONLIST (MAPCAR ASSERTIONLIST
                                    (FUNCTION (LAMBDA (CONTEXTASSERTS)
                                        (CONS ASSERTION CONTEXTASSERTS]
      ((OR (EQ CONTEXT (QUOTE CURRENT))
           (NULL CONTEXT))
        (SETQ ASSERTIONLIST (CONS (CONS ASSERTION (CAR ASSERTIONLIST))
                                  (CDR ASSERTIONLIST])

(BRUTE
  [LAMBDA (CODE SYNTHLIST)
    (PROG (SYNTH)
          (COND
            ((NULL CODE)
              NIL)
            ((SETQ SYNTH (CONSSYNTH CODE SYNTHLIST))
              SYNTH)
            ((SETQ SYNTH (CDR (SASSOC CODE SYNTHLIST)))
              SYNTH)
            ((ATOM CODE)
              (QUOTE FAILATOM))
            (T (CONS (QUOTE LIST)
                     (MAPCAR CODE (FUNCTION (LAMBDA (CODEL)
                                 (BRUTE CODEL (PRUNEARGS (FLATTEN
                                                           CODEL)
                                                         SYNTHLIST])

(BRUTESYNTH
  [LAMBDA (CODE SYNTHLIST)
    (COND
      ([NOFAILS (SETQ SYNTHESIS (BRUTE CODE (PRUNEARGS CODE SYNTHLIST]
        SYNTHESIS)
      (T (QUOTE *FAIL])

(CONSSYNTH
  [LAMBDA (CODE SYNTHLIST)
    (PROG (CARSYNTH CDRSYNTH)
          (COND
            ([AND (SETQ CDRSYNTH (CDR (SASSOC (CDR CODE)
                                              SYNTHLIST)))
                  (NOFAILS (SETQ CARSYNTH
                             (BRUTE (CAR CODE)
                                    (PRUNEARGS (FLATTEN (CAR CODE))
                                               SYNTHLIST]
              (LIST (QUOTE CONS)
                    CARSYNTH CDRSYNTH])

(DIFTEMPFN
  [LAMBDA (ELFORM1 ELFORM2)
    (COND
      [(NULL ELFORM1)
        (COND
          ((NULL ELFORM2)
            NIL)
          (T (QUOTE FAILATOM]
      ((NULL ELFORM2)
        (QUOTE FAILATOM))
      ((EQUAL ELFORM1 ELFORM2)
        ELFORM1)
      ((OR (ATOM ELFORM1)
           (ATOM ELFORM2))
        (COND
          ((AND (NUMBERP ELFORM1)
                (NUMBERP ELFORM2))
            (SETQ GENVA (GENSYM))
            [PUT GENVA (QUOTE TRANS)
                 (PROGN (SETQ DIFF (IDIFFERENCE ELFORM2 ELFORM1))
                        (COND
                          ((EQ DIFF 1)
                            (QUOTE (ADD1 *LAST)))
                          ((EQ DIFF -1)
                            (QUOTE (SUB1 *LAST)))
                          (T (LIST (QUOTE IPLUS)
                                   (QUOTE *LAST)
                                   DIFF]
            GENVA)))
      (T (DOUBLEMAPCAR ELFORM1 ELFORM2 (FUNCTION DIFTEMPFN])

(DIFTEMPFUN
  [LAMBDA (ELFORM1 ELFORM2)
    (COND
      ((NOFAILS (DIFTEMPFN ELFORM1 ELFORM2)))
      (T (QUOTE *FAIL])

(DOUBLEMAPCAR
  [LAMBDA (LIST1 LIST2 FN)
    (COND
      ((NULL LIST1)
        NIL)
      (T (CONS (APPLY FN (LIST (CAR LIST1)
                               (CAR LIST2)))
               (DOUBLEMAPCAR (CDR LIST1)
                             (CDR LIST2)
                             FN])

(ELFORM
  [LAMBDA (SYNTHESIS)
    (COND
      ((EQ (CAR SYNTHESIS)
           (QUOTE ARG))
        SYNTHESIS)
      ((EQ (CAR SYNTHESIS)
           (QUOTE CAR))
        (ELFORM1 (CADR SYNTHESIS)
                 1))
      (T (PRINT SYNTHESIS)
         (PRINT (QUOTE (IS NOT IN PROPER FORM TO BE CONVERTED
                          TO ELFORM])

(ELFORM1
  [LAMBDA (SYNTHESIS NUM)
    (COND
      ((EQ (CAR SYNTHESIS)
           (QUOTE ARG))
        (LIST (QUOTE EL)
              NUM SYNTHESIS))
      ((EQ (CAR SYNTHESIS)
           (QUOTE CDR))
        (ELFORM1 (CADR SYNTHESIS)
                 (ADD1 NUM)))
      (T (PRINT (QUOTE (NOT IN ELFORM])

(ELNUM
  [LAMBDA (EL LIST)
    (COND
      ((NULL LIST)
        NIL)
      ((EQ EL (CAR LIST))
        1)
      (T (COND
           ((SETQ NUMB (ELNUM EL (CDR LIST)))
             (ADD1 NUMB))
           (T NIL])

(FILECREATED
  [NLAMBDA ZZZ NIL])

(FINDVARIABLE
  [LAMBDA (VAR SYNTHLIST)
    [COND
      ((NULL SYNTHLIST)
        (QUOTE FAILATOM))
      (T (MAPC SYNTHLIST
               (FUNCTION (LAMBDA (SYNTHPAIR)
                   (COND
                     ([AND (EQUAL VAR (CAR SYNTHPAIR))
                           (NOT (EQUAL (SETQ DESCRIP
                                         (ELFORM (CDR SYNTHPAIR)))
                                       (QUOTE *FAIL]
                       (SETQ ELDESCRIP DESCRIP))
                     ([AND (SETQ ELNUMBER (ELNUM VAR (CAR SYNTHPAIR)))
                           (SETQ DESCRIP (ELFORM (CDR SYNTHPAIR]
                       (SETQ ELDESCRIP (LIST (QUOTE EL)
                                             ELNUMBER DESCRIP)))
                     (T (SETQ ELDESCRIP (QUOTE FAILATOM]
    ELDESCRIP])

(FLATTEN
  [LAMBDA (LIST)
    (COND
      ((NULL LIST)
        NIL)
      ((ATOM LIST)
        (LIST LIST))
      (T (APPEND (FLATTEN (CAR LIST))
                 (FLATTEN (CDR LIST])

(NOFAILS
  [LAMBDA (LIST)
    (COND
      ((NOT (MEMB (QUOTE FAILATOM)
                  (FLATTEN LIST)))
        LIST])

(POPCONTEXT
  [LAMBDA NIL
    (SETQ ASSERTIONLIST (CDR ASSERTIONLIST])

(PRUNEARGS
  [LAMBDA (CODEATOMS SYNTHLIST)
    (COND
      ((NULL SYNTHLIST)
        NIL)
      [[EVERY (FLATTEN (CAAR SYNTHLIST))
              (FUNCTION (LAMBDA (ARGATOM)
                  (MEMB ARGATOM CODEATOMS]
        (CONS (CAR SYNTHLIST)
              (PRUNEARGS CODEATOMS (CDR SYNTHLIST]
      (T (PRUNEARGS CODEATOMS (CDR SYNTHLIST])

(PUSHCONTEXT
  [LAMBDA NIL
    (SETQ ASSERTIONLIST (CONS NIL ASSERTIONLIST])

(TEMP
  [LAMBDA (FIRST SECOND SYNTHLIST)
    (COND
      ((NOFAILS (TEMPLATE FIRST SECOND SYNTHLIST)))
      (T (QUOTE *FAIL])

(TEMPLATE
  [LAMBDA (FIRST SECOND SYNTHLIST)
    (COND
      [(NULL FIRST)
        (COND
          ((NULL SECOND)
            NIL)
          (T (LIST (QUOTE FAILATOM]
      ((NULL SECOND)
        (LIST (QUOTE FAILATOM)))
      ((EQUAL FIRST SECOND)
        FIRST)
      ((OR (ATOM FIRST)
           (ATOM SECOND))
        (SETQ GENVAR (GENSYM))
        (PUT GENVAR (QUOTE VARIABLE)
             T)
        [PUT GENVAR (QUOTE DIFTEMP)
             (DIFTEMPFN (PUT GENVAR (QUOTE INST1)
                             (FINDVARIABLE FIRST SYNTHLIST))
                        (PUT GENVAR (QUOTE INST2)
                             (FINDVARIABLE SECOND SYNTHLIST]
        GENVAR)
      (T (DOUBLEMAPCAR FIRST SECOND (FUNCTION (LAMBDA (EL1 EL2)
                           (TEMPLATE EL1 EL2 SYNTHLIST])
)
  (LISPXPRINT (QUOTE EXAMFNS)
              T)
  (RPAQQ EXAMFNS
         (ADDFNS ASSERT BRUTE BRUTESYNTH CONSSYNTH DIFTEMPFN DIFTEMPFUN 
                 DOUBLEMAPCAR ELFORM ELFORM1 ELNUM FILECREATED 
                 FINDVARIABLE FLATTEN NOFAILS POPCONTEXT PRUNEARGS 
                 PUSHCONTEXT TEMP TEMPLATE))
  (LISPXPRINT (QUOTE EXAMVARS)
              T)
  (RPAQQ EXAMVARS (CODE SYN))
  (RPAQQ CODE (A E F))
  (RPAQQ SYN (((A B C D)
           ARG 1)))
STOP